数据通路与控制通路模块的形式等价验证
SNUG China 2022
2022
29 页
数据通路与控制通路模块的形式等价验证
会议: SNUG China 2022 | 作者: Li Haoran | 页数: 29 (116 张图片)
第1-2页
三种形式等价检查方法对比： - 布尔等价（Formality）：匹配比较点，比较布尔扇入逻辑 - 时序等价（VC Formal SEQ）：假设相等输入和起始状态，在每个周期比较无界输出 - 事务等价（VC Formal DPV）：非定时事务模型A vs 周期精确模型B，假设相等输入，在事务结束时比较输出
第3-15页 — 形式等价检查
VC Formal DPV用于算术模块：支持C/C++算法模型与RTL之间的等价验证，特别适合数据通路密集型设计（如FIR滤波器、FFT）。关键挑战是处理流水线深度不匹配和时序重排。
第16-25页 — VC Formal SEQ用于自动时钟门控
自动时钟门控插入后需验证功能等价性。SEQ可验证时钟门控优化前后的设计在无界时间内对所有可达状态产生相同输出。处理的关键：门控使能条件、门控锁存器透明性、X-乐观问题。
第26-29页 — 结论与问答
形式等价验证在大型SoC设计中弥补了仿真覆盖率缺口。VC Formal DPV适合数据通路，SEQ适合控制通路（含时钟门控），Formality适合门级vs RTL的布尔等价。